WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2} / {0/0,dd/2,false/0,nil/0,pair/2
            ,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,bubble,bubble',bubble'',bubblesort,bubblesort'
            ,lt} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
          append#(nil(),ys) -> c_2()
          bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
          bubble#(dd(x,nil())) -> c_4()
          bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs)))
          bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs)))
          bubble''#(x,pair(xs,x')) -> c_7()
          bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
          bubblesort#(nil()) -> c_9()
          bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
          lt#(0(),0()) -> c_11()
          lt#(0(),s(y)) -> c_12()
          lt#(s(x),0()) -> c_13()
          lt#(s(x),s(y)) -> c_14(lt#(x,y))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            append#(nil(),ys) -> c_2()
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
            bubble#(dd(x,nil())) -> c_4()
            bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs)))
            bubble''#(x,pair(xs,x')) -> c_7()
            bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
            bubblesort#(nil()) -> c_9()
            bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
            lt#(0(),0()) -> c_11()
            lt#(0(),s(y)) -> c_12()
            lt#(s(x),0()) -> c_13()
            lt#(s(x),s(y)) -> c_14(lt#(x,y))
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/2,c_6/2,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,7,9,11,12,13}
        by application of
          Pre({2,4,7,9,11,12,13}) = {1,3,5,6,8,10,14}.
        Here rules are labelled as follows:
          1: append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
          2: append#(nil(),ys) -> c_2()
          3: bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
          4: bubble#(dd(x,nil())) -> c_4()
          5: bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs)))
          6: bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs)))
          7: bubble''#(x,pair(xs,x')) -> c_7()
          8: bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
          9: bubblesort#(nil()) -> c_9()
          10: bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
          11: lt#(0(),0()) -> c_11()
          12: lt#(0(),s(y)) -> c_12()
          13: lt#(s(x),0()) -> c_13()
          14: lt#(s(x),s(y)) -> c_14(lt#(x,y))
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
            bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs)))
            bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
            lt#(s(x),s(y)) -> c_14(lt#(x,y))
        - Weak DPs:
            append#(nil(),ys) -> c_2()
            bubble#(dd(x,nil())) -> c_4()
            bubble''#(x,pair(xs,x')) -> c_7()
            bubblesort#(nil()) -> c_9()
            lt#(0(),0()) -> c_11()
            lt#(0(),s(y)) -> c_12()
            lt#(s(x),0()) -> c_13()
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/2,c_6/2,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
             -->_1 append#(nil(),ys) -> c_2():8
             -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          2:S:bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
             -->_2 lt#(s(x),s(y)) -> c_14(lt#(x,y)):7
             -->_1 bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs))):4
             -->_1 bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs))):3
             -->_2 lt#(s(x),0()) -> c_13():14
             -->_2 lt#(0(),s(y)) -> c_12():13
             -->_2 lt#(0(),0()) -> c_11():12
          
          3:S:bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs)))
             -->_1 bubble''#(x,pair(xs,x')) -> c_7():10
             -->_2 bubble#(dd(x,nil())) -> c_4():9
             -->_2 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          4:S:bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs)))
             -->_1 bubble''#(x,pair(xs,x')) -> c_7():10
             -->_2 bubble#(dd(x,nil())) -> c_4():9
             -->_2 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          5:S:bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
             -->_1 bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs)):6
             -->_2 bubble#(dd(x,nil())) -> c_4():9
             -->_2 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          6:S:bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
             -->_2 bubblesort#(nil()) -> c_9():11
             -->_1 append#(nil(),ys) -> c_2():8
             -->_2 bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs))):5
             -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          7:S:lt#(s(x),s(y)) -> c_14(lt#(x,y))
             -->_1 lt#(s(x),0()) -> c_13():14
             -->_1 lt#(0(),s(y)) -> c_12():13
             -->_1 lt#(0(),0()) -> c_11():12
             -->_1 lt#(s(x),s(y)) -> c_14(lt#(x,y)):7
          
          8:W:append#(nil(),ys) -> c_2()
             
          
          9:W:bubble#(dd(x,nil())) -> c_4()
             
          
          10:W:bubble''#(x,pair(xs,x')) -> c_7()
             
          
          11:W:bubblesort#(nil()) -> c_9()
             
          
          12:W:lt#(0(),0()) -> c_11()
             
          
          13:W:lt#(0(),s(y)) -> c_12()
             
          
          14:W:lt#(s(x),0()) -> c_13()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          11: bubblesort#(nil()) -> c_9()
          9: bubble#(dd(x,nil())) -> c_4()
          10: bubble''#(x,pair(xs,x')) -> c_7()
          12: lt#(0(),0()) -> c_11()
          13: lt#(0(),s(y)) -> c_12()
          14: lt#(s(x),0()) -> c_13()
          8: append#(nil(),ys) -> c_2()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
            bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs)))
            bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
            lt#(s(x),s(y)) -> c_14(lt#(x,y))
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/2,c_6/2,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
             -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          2:S:bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
             -->_2 lt#(s(x),s(y)) -> c_14(lt#(x,y)):7
             -->_1 bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs))):4
             -->_1 bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs))):3
          
          3:S:bubble'#(false(),x,x',xs) -> c_5(bubble''#(x',bubble(dd(x,xs))),bubble#(dd(x,xs)))
             -->_2 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          4:S:bubble'#(true(),x,x',xs) -> c_6(bubble''#(x,bubble(dd(x',xs))),bubble#(dd(x',xs)))
             -->_2 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          5:S:bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
             -->_1 bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs)):6
             -->_2 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          6:S:bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
             -->_2 bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs))):5
             -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          7:S:lt#(s(x),s(y)) -> c_14(lt#(x,y))
             -->_1 lt#(s(x),s(y)) -> c_14(lt#(x,y)):7
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
          bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
* Step 5: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
            bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
            bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
            lt#(s(x),s(y)) -> c_14(lt#(x,y))
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
          bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
        and a lower component
          append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
          bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
          bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
          bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
          lt#(s(x),s(y)) -> c_14(lt#(x,y))
        Further, following extension rules are added to the lower component.
          bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
          bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
          bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
          bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
** Step 5.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs)))
             -->_1 bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs)):2
          
          2:S:bubblesort'#(pair(xs,x)) -> c_10(append#(bubblesort(xs),dd(x,nil())),bubblesort#(xs))
             -->_2 bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))),bubble#(dd(x,xs))):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))))
          bubblesort'#(pair(xs,x)) -> c_10(bubblesort#(xs))
** Step 5.a:2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))))
            bubblesort'#(pair(xs,x)) -> c_10(bubblesort#(xs))
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
          bubble(dd(x,nil())) -> pair(nil(),x)
          bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
          bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
          bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
          lt(0(),0()) -> false()
          lt(0(),s(y)) -> true()
          lt(s(x),0()) -> false()
          lt(s(x),s(y)) -> lt(x,y)
          bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))))
          bubblesort'#(pair(xs,x)) -> c_10(bubblesort#(xs))
** Step 5.a:3: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))))
            bubblesort'#(pair(xs,x)) -> c_10(bubblesort#(xs))
        - Weak TRS:
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0)
          bubble :: ["A"(5)] -(0)-> "A"(5)
          bubble' :: ["A"(0) x "A"(5) x "A"(5) x "A"(5)] -(10)-> "A"(5)
          bubble'' :: ["A"(5) x "A"(5)] -(5)-> "A"(5)
          dd :: ["A"(5) x "A"(5)] -(5)-> "A"(5)
          false :: [] -(0)-> "A"(0)
          false :: [] -(0)-> "A"(15)
          lt :: ["A"(0) x "A"(0)] -(0)-> "A"(15)
          nil :: [] -(0)-> "A"(5)
          nil :: [] -(0)-> "A"(15)
          pair :: ["A"(5) x "A"(0)] -(5)-> "A"(5)
          s :: ["A"(0)] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(15)
          bubblesort# :: ["A"(5)] -(14)-> "A"(1)
          bubblesort'# :: ["A"(5)] -(10)-> "A"(13)
          c_8 :: ["A"(0)] -(0)-> "A"(15)
          c_10 :: ["A"(0)] -(0)-> "A"(15)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1)
          "c_10_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_8_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
          "false_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "pair_A" :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          "s_A" :: ["A"(1)] -(1)-> "A"(1)
          "true_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          bubblesort'#(pair(xs,x)) -> c_10(bubblesort#(xs))
        2. Weak:
          bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))))
** Step 5.a:4: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))))
        - Weak DPs:
            bubblesort'#(pair(xs,x)) -> c_10(bubblesort#(xs))
        - Weak TRS:
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0)
          bubble :: ["A"(1)] -(0)-> "A"(1)
          bubble' :: ["A"(1) x "A"(0) x "A"(0) x "A"(1)] -(2)-> "A"(1)
          bubble'' :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          false :: [] -(0)-> "A"(1)
          false :: [] -(0)-> "A"(15)
          lt :: ["A"(0) x "A"(0)] -(0)-> "A"(15)
          nil :: [] -(0)-> "A"(1)
          nil :: [] -(0)-> "A"(15)
          pair :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          s :: ["A"(0)] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(1)
          true :: [] -(0)-> "A"(15)
          bubblesort# :: ["A"(1)] -(2)-> "A"(1)
          bubblesort'# :: ["A"(1)] -(1)-> "A"(13)
          c_8 :: ["A"(11)] -(0)-> "A"(11)
          c_10 :: ["A"(0)] -(0)-> "A"(15)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1)
          "c_10_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_8_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "false_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "pair_A" :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          "s_A" :: ["A"(1)] -(1)-> "A"(1)
          "true_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          bubblesort#(dd(x,xs)) -> c_8(bubblesort'#(bubble(dd(x,xs))))
        2. Weak:
          

** Step 5.b:1: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
            bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
            lt#(s(x),s(y)) -> c_14(lt#(x,y))
        - Weak DPs:
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
          bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
          bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
          bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
          bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
          bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
          bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
          bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        and a lower component
          lt#(s(x),s(y)) -> c_14(lt#(x,y))
        Further, following extension rules are added to the lower component.
          append#(dd(x,xs),ys) -> append#(xs,ys)
          bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs)
          bubble#(dd(x,dd(x',xs))) -> lt#(x,x')
          bubble'#(false(),x,x',xs) -> bubble#(dd(x,xs))
          bubble'#(true(),x,x',xs) -> bubble#(dd(x',xs))
          bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
          bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
          bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
          bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
*** Step 5.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
            bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
        - Weak DPs:
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
             -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          2:S:bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x'))
             -->_1 bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs))):4
             -->_1 bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs))):3
          
          3:S:bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
             -->_1 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          4:S:bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
             -->_1 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          5:W:bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
             -->_1 bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs),lt#(x,x')):2
          
          6:W:bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
             -->_1 bubblesort'#(pair(xs,x)) -> bubblesort#(xs):8
             -->_1 bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil())):7
          
          7:W:bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
             -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          8:W:bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
             -->_1 bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs))):6
             -->_1 bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs)):5
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs))
*** Step 5.b:1.a:2: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs))
            bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
        - Weak DPs:
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0)
          append :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
          bubble :: ["A"(7)] -(1)-> "A"(7)
          bubble' :: ["A"(1) x "A"(0) x "A"(0) x "A"(7)] -(15)-> "A"(7)
          bubble'' :: ["A"(0) x "A"(7)] -(7)-> "A"(7)
          bubblesort :: ["A"(7)] -(7)-> "A"(1)
          bubblesort' :: ["A"(7)] -(4)-> "A"(1)
          dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          dd :: ["A"(0) x "A"(7)] -(7)-> "A"(7)
          dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          false :: [] -(0)-> "A"(1)
          false :: [] -(0)-> "A"(15)
          lt :: ["A"(0) x "A"(0)] -(0)-> "A"(9)
          nil :: [] -(0)-> "A"(1)
          nil :: [] -(0)-> "A"(7)
          nil :: [] -(0)-> "A"(15)
          pair :: ["A"(7) x "A"(0)] -(7)-> "A"(7)
          pair :: ["A"(8) x "A"(0)] -(8)-> "A"(8)
          s :: ["A"(0)] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(1)
          true :: [] -(0)-> "A"(15)
          append# :: ["A"(1) x "A"(0)] -(0)-> "A"(8)
          bubble# :: ["A"(7)] -(2)-> "A"(5)
          bubble'# :: ["A"(1) x "A"(0) x "A"(0) x "A"(7)] -(9)-> "A"(13)
          bubblesort# :: ["A"(7)] -(4)-> "A"(4)
          bubblesort'# :: ["A"(7)] -(0)-> "A"(4)
          c_1 :: ["A"(0)] -(0)-> "A"(12)
          c_3 :: ["A"(0)] -(0)-> "A"(12)
          c_5 :: ["A"(0)] -(0)-> "A"(15)
          c_6 :: ["A"(0)] -(0)-> "A"(15)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1)
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_5_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_6_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "false_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "pair_A" :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          "s_A" :: ["A"(0)] -(0)-> "A"(1)
          "true_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
        2. Weak:
          bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs))
          bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
          bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
*** Step 5.b:1.a:3: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs))
            bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
        - Weak DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0)
          append :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          bubble :: ["A"(1)] -(0)-> "A"(1)
          bubble' :: ["A"(1) x "A"(0) x "A"(0) x "A"(1)] -(2)-> "A"(1)
          bubble'' :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          bubblesort :: ["A"(1)] -(0)-> "A"(0)
          bubblesort' :: ["A"(1)] -(0)-> "A"(0)
          dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          false :: [] -(0)-> "A"(1)
          false :: [] -(0)-> "A"(15)
          lt :: ["A"(0) x "A"(0)] -(0)-> "A"(9)
          nil :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(1)
          nil :: [] -(0)-> "A"(15)
          nil :: [] -(0)-> "A"(7)
          pair :: ["A"(1) x "A"(0)] -(0)-> "A"(1)
          pair :: ["A"(8) x "A"(0)] -(0)-> "A"(8)
          s :: ["A"(0)] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(1)
          true :: [] -(0)-> "A"(15)
          append# :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          bubble# :: ["A"(1)] -(0)-> "A"(1)
          bubble'# :: ["A"(1) x "A"(0) x "A"(0) x "A"(1)] -(1)-> "A"(2)
          bubblesort# :: ["A"(1)] -(6)-> "A"(0)
          bubblesort'# :: ["A"(1)] -(6)-> "A"(0)
          c_1 :: ["A"(0)] -(0)-> "A"(12)
          c_3 :: ["A"(0)] -(0)-> "A"(3)
          c_5 :: ["A"(0)] -(0)-> "A"(14)
          c_6 :: ["A"(0)] -(0)-> "A"(3)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1)
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_5_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_6_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "false_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "pair_A" :: ["A"(1) x "A"(0)] -(0)-> "A"(1)
          "s_A" :: ["A"(1)] -(1)-> "A"(1)
          "true_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs))
        2. Weak:
          bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
          bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
*** Step 5.b:1.a:4: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
            bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
        - Weak DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs))
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0)
          append :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          bubble :: ["A"(1)] -(1)-> "A"(1)
          bubble' :: ["A"(1) x "A"(0) x "A"(0) x "A"(1)] -(3)-> "A"(1)
          bubble'' :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          bubblesort :: ["A"(1)] -(15)-> "A"(0)
          bubblesort' :: ["A"(1)] -(14)-> "A"(0)
          dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          false :: [] -(0)-> "A"(0)
          false :: [] -(0)-> "A"(1)
          false :: [] -(0)-> "A"(13)
          lt :: ["A"(0) x "A"(0)] -(0)-> "A"(11)
          nil :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(1)
          nil :: [] -(0)-> "A"(15)
          nil :: [] -(0)-> "A"(7)
          pair :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          s :: ["A"(0)] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(1)
          true :: [] -(0)-> "A"(13)
          append# :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          bubble# :: ["A"(1)] -(0)-> "A"(2)
          bubble'# :: ["A"(0) x "A"(0) x "A"(0) x "A"(1)] -(2)-> "A"(4)
          bubblesort# :: ["A"(1)] -(15)-> "A"(1)
          bubblesort'# :: ["A"(1)] -(14)-> "A"(1)
          c_1 :: ["A"(0)] -(0)-> "A"(12)
          c_3 :: ["A"(0)] -(0)-> "A"(15)
          c_5 :: ["A"(0)] -(0)-> "A"(14)
          c_6 :: ["A"(0)] -(0)-> "A"(15)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1)
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_5_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_6_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "false_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "pair_A" :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          "s_A" :: ["A"(1)] -(1)-> "A"(1)
          "true_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
        2. Weak:
          bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
*** Step 5.b:1.a:5: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
        - Weak DPs:
            append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
            bubble#(dd(x,dd(x',xs))) -> c_3(bubble'#(lt(x,x'),x,x',xs))
            bubble'#(false(),x,x',xs) -> c_5(bubble#(dd(x,xs)))
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0)
          append :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          bubble :: ["A"(4)] -(0)-> "A"(4)
          bubble' :: ["A"(1) x "A"(0) x "A"(0) x "A"(4)] -(8)-> "A"(4)
          bubble'' :: ["A"(0) x "A"(4)] -(4)-> "A"(4)
          bubblesort :: ["A"(4)] -(12)-> "A"(0)
          bubblesort' :: ["A"(4)] -(12)-> "A"(0)
          dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          dd :: ["A"(0) x "A"(4)] -(4)-> "A"(4)
          dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          false :: [] -(0)-> "A"(1)
          false :: [] -(0)-> "A"(0)
          false :: [] -(0)-> "A"(13)
          lt :: ["A"(0) x "A"(0)] -(0)-> "A"(11)
          nil :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(4)
          nil :: [] -(0)-> "A"(15)
          nil :: [] -(0)-> "A"(7)
          pair :: ["A"(4) x "A"(0)] -(0)-> "A"(4)
          s :: ["A"(0)] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(1)
          true :: [] -(0)-> "A"(13)
          append# :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          bubble# :: ["A"(4)] -(0)-> "A"(13)
          bubble'# :: ["A"(0) x "A"(0) x "A"(0) x "A"(4)] -(8)-> "A"(9)
          bubblesort# :: ["A"(4)] -(14)-> "A"(1)
          bubblesort'# :: ["A"(4)] -(14)-> "A"(1)
          c_1 :: ["A"(0)] -(0)-> "A"(12)
          c_3 :: ["A"(0)] -(0)-> "A"(15)
          c_5 :: ["A"(13)] -(0)-> "A"(13)
          c_6 :: ["A"(0)] -(0)-> "A"(12)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1)
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_5_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_6_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "false_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "pair_A" :: ["A"(1) x "A"(0)] -(0)-> "A"(1)
          "s_A" :: ["A"(1)] -(1)-> "A"(1)
          "true_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          bubble'#(true(),x,x',xs) -> c_6(bubble#(dd(x',xs)))
        2. Weak:
          

*** Step 5.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            lt#(s(x),s(y)) -> c_14(lt#(x,y))
        - Weak DPs:
            append#(dd(x,xs),ys) -> append#(xs,ys)
            bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs)
            bubble#(dd(x,dd(x',xs))) -> lt#(x,x')
            bubble'#(false(),x,x',xs) -> bubble#(dd(x,xs))
            bubble'#(true(),x,x',xs) -> bubble#(dd(x',xs))
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:lt#(s(x),s(y)) -> c_14(lt#(x,y))
             -->_1 lt#(s(x),s(y)) -> c_14(lt#(x,y)):1
          
          2:W:append#(dd(x,xs),ys) -> append#(xs,ys)
             -->_1 append#(dd(x,xs),ys) -> append#(xs,ys):2
          
          3:W:bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs)
             -->_1 bubble'#(true(),x,x',xs) -> bubble#(dd(x',xs)):6
             -->_1 bubble'#(false(),x,x',xs) -> bubble#(dd(x,xs)):5
          
          4:W:bubble#(dd(x,dd(x',xs))) -> lt#(x,x')
             -->_1 lt#(s(x),s(y)) -> c_14(lt#(x,y)):1
          
          5:W:bubble'#(false(),x,x',xs) -> bubble#(dd(x,xs))
             -->_1 bubble#(dd(x,dd(x',xs))) -> lt#(x,x'):4
             -->_1 bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs):3
          
          6:W:bubble'#(true(),x,x',xs) -> bubble#(dd(x',xs))
             -->_1 bubble#(dd(x,dd(x',xs))) -> lt#(x,x'):4
             -->_1 bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs):3
          
          7:W:bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
             -->_1 bubble#(dd(x,dd(x',xs))) -> lt#(x,x'):4
             -->_1 bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs):3
          
          8:W:bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
             -->_1 bubblesort'#(pair(xs,x)) -> bubblesort#(xs):10
             -->_1 bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil())):9
          
          9:W:bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
             -->_1 append#(dd(x,xs),ys) -> append#(xs,ys):2
          
          10:W:bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
             -->_1 bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs))):8
             -->_1 bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs)):7
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          9: bubblesort'#(pair(xs,x)) -> append#(bubblesort(xs),dd(x,nil()))
          2: append#(dd(x,xs),ys) -> append#(xs,ys)
*** Step 5.b:1.b:2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            lt#(s(x),s(y)) -> c_14(lt#(x,y))
        - Weak DPs:
            bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs)
            bubble#(dd(x,dd(x',xs))) -> lt#(x,x')
            bubble'#(false(),x,x',xs) -> bubble#(dd(x,xs))
            bubble'#(true(),x,x',xs) -> bubble#(dd(x',xs))
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            append(dd(x,xs),ys) -> dd(x,append(xs,ys))
            append(nil(),ys) -> ys
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            bubblesort(dd(x,xs)) -> bubblesort'(bubble(dd(x,xs)))
            bubblesort(nil()) -> nil()
            bubblesort'(pair(xs,x)) -> append(bubblesort(xs),dd(x,nil()))
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
          bubble(dd(x,nil())) -> pair(nil(),x)
          bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
          bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
          bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
          lt(0(),0()) -> false()
          lt(0(),s(y)) -> true()
          lt(s(x),0()) -> false()
          lt(s(x),s(y)) -> lt(x,y)
          bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs)
          bubble#(dd(x,dd(x',xs))) -> lt#(x,x')
          bubble'#(false(),x,x',xs) -> bubble#(dd(x,xs))
          bubble'#(true(),x,x',xs) -> bubble#(dd(x',xs))
          bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
          bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
          bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
          lt#(s(x),s(y)) -> c_14(lt#(x,y))
*** Step 5.b:1.b:3: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            lt#(s(x),s(y)) -> c_14(lt#(x,y))
        - Weak DPs:
            bubble#(dd(x,dd(x',xs))) -> bubble'#(lt(x,x'),x,x',xs)
            bubble#(dd(x,dd(x',xs))) -> lt#(x,x')
            bubble'#(false(),x,x',xs) -> bubble#(dd(x,xs))
            bubble'#(true(),x,x',xs) -> bubble#(dd(x',xs))
            bubblesort#(dd(x,xs)) -> bubble#(dd(x,xs))
            bubblesort#(dd(x,xs)) -> bubblesort'#(bubble(dd(x,xs)))
            bubblesort'#(pair(xs,x)) -> bubblesort#(xs)
        - Weak TRS:
            bubble(dd(x,dd(x',xs))) -> bubble'(lt(x,x'),x,x',xs)
            bubble(dd(x,nil())) -> pair(nil(),x)
            bubble'(false(),x,x',xs) -> bubble''(x',bubble(dd(x,xs)))
            bubble'(true(),x,x',xs) -> bubble''(x,bubble(dd(x',xs)))
            bubble''(x,pair(xs,x')) -> pair(dd(x,xs),x')
            lt(0(),0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),0()) -> false()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {append/2,bubble/1,bubble'/4,bubble''/2,bubblesort/1,bubblesort'/1,lt/2,append#/2,bubble#/1,bubble'#/4
            ,bubble''#/2,bubblesort#/1,bubblesort'#/1,lt#/2} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0
            ,c_3/2,c_4/0,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,bubble#,bubble'#,bubble''#,bubblesort#
            ,bubblesort'#,lt#} and constructors {0,dd,false,nil,pair,s,true}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0)
          bubble :: ["A"(11)] -(11)-> "A"(11)
          bubble' :: ["A"(1) x "A"(11) x "A"(11) x "A"(11)] -(11)-> "A"(11)
          bubble'' :: ["A"(11) x "A"(11)] -(0)-> "A"(11)
          dd :: ["A"(11) x "A"(11)] -(0)-> "A"(11)
          false :: [] -(0)-> "A"(1)
          false :: [] -(0)-> "A"(15)
          lt :: ["A"(0) x "A"(0)] -(0)-> "A"(13)
          nil :: [] -(0)-> "A"(11)
          nil :: [] -(0)-> "A"(15)
          pair :: ["A"(11) x "A"(0)] -(11)-> "A"(11)
          s :: ["A"(11)] -(11)-> "A"(11)
          s :: ["A"(0)] -(0)-> "A"(0)
          true :: [] -(0)-> "A"(1)
          true :: [] -(0)-> "A"(15)
          bubble# :: ["A"(11)] -(12)-> "A"(1)
          bubble'# :: ["A"(1) x "A"(11) x "A"(11) x "A"(11)] -(12)-> "A"(1)
          bubblesort# :: ["A"(11)] -(12)-> "A"(0)
          bubblesort'# :: ["A"(11)] -(1)-> "A"(0)
          lt# :: ["A"(11) x "A"(11)] -(11)-> "A"(3)
          c_14 :: ["A"(0)] -(0)-> "A"(15)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1)
          "c_14_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
          "false_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "pair_A" :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          "s_A" :: ["A"(1)] -(1)-> "A"(1)
          "true_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          lt#(s(x),s(y)) -> c_14(lt#(x,y))
        2. Weak:
          

WORST_CASE(?,O(n^3))